(declare-sort T)

(declare-fun b () (Array Int Int))
(declare-fun c () (Array Int Int))
(declare-fun j () Int)
(assert (and (not (= b c)) (= 0 (select c 0)) (= b (store c 1 0)) (= c (store c j 0))))
(check-sat)
(declare-const s1 (Set (List Int)))
(declare-const s2 (Set (List Int)))
(declare-const s3 (Set (List Int)))
(assert (not (= s1 s3)))
(assert (= s1 ((_ map and) s2 s3)))
(declare-fun subtype (T T) Bool)
(assert (forall ((x T) (y T) (z T)) (and (subtype x y) (subtype y z))))
(declare-const string-type T)
(assert (subtype string-type string-type))
(check-sat)
